﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Collections.ObjectModel;

namespace OpSatPlan.Encoder
{
    public class CnfVariables
    {
        private List<Dictionary<AtomicFormula, int>> mPredicateVariableMap;
        private List<Dictionary<Operator, int>> mActionVariableMap;
		private Dictionary<int, Operator> mReversActionMap;
		private Dictionary<int, AtomicFormula> mReversePredicateMap;
		private Dictionary<int, int> mTimeStepMap;
        private int mSatVariable;
        public CnfVariables()
        {
            this.mPredicateVariableMap = new List<Dictionary<AtomicFormula, int>>();
            this.mActionVariableMap = new List<Dictionary<Operator, int>>();
			this.mReversActionMap = new Dictionary<int, Operator>();
			this.mReversePredicateMap = new Dictionary<int, AtomicFormula>();
			this.mTimeStepMap = new Dictionary<int, int>();
            this.mSatVariable = 1;
        }

        public int NumberOfVariables
        {
            get
            {
                return this.mSatVariable - 1;
            }
        }

        public void Reset()
        {
            this.mPredicateVariableMap.Clear();
            this.mActionVariableMap.Clear();
			this.mReversActionMap.Clear();
			this.mReversePredicateMap.Clear();
			this.mTimeStepMap.Clear();
            this.mSatVariable = 1;
        }

        public int GetVariable(Operator op, int level)
        {
            int i = level;

            Dictionary<Operator, int> map;
            while (level >= this.mActionVariableMap.Count)
            {
                this.mActionVariableMap.Add(new Dictionary<Operator, int>());
                i++;
            }

            map = this.mActionVariableMap[level];

            if (map.ContainsKey(op))
            {
                return map[op];
            }
            else
            {
				this.mTimeStepMap.Add(this.mSatVariable, level);
                map.Add(op, this.mSatVariable);
				this.mReversActionMap.Add(this.mSatVariable, op);
                this.mSatVariable++;
                return map[op];
            }
        }
        public int GetVariable(ValuedAtomicFormula vaf, int level)
        {
            return this.GetVariable(vaf.AtomicFormula, level);
        }

        public bool CheckVariable(ValuedAtomicFormula vaf, int level)
        {
            return this.CheckVariable(vaf.AtomicFormula, level);
        }
        public bool CheckVariable(AtomicFormula af, int level)
        {
            if (this.mPredicateVariableMap.Count <= level)
            {
                return false;
            }
            return this.mPredicateVariableMap[level].ContainsKey(af);
        }
        public int GetVariable(AtomicFormula af, int level)
        {
            int i = level;
            Dictionary<AtomicFormula, int> map;
			
            while (level >= this.mPredicateVariableMap.Count)
            {
                this.mPredicateVariableMap.Add(new Dictionary<AtomicFormula, int>());
                i++;
            }

            map = this.mPredicateVariableMap[level];

            if (map.ContainsKey(af))
            {
                return map[af];
            }
            else
            {
				this.mTimeStepMap.Add(this.mSatVariable, level);
                map.Add(af, this.mSatVariable);
				this.mReversePredicateMap.Add(this.mSatVariable, af);
                this.mSatVariable++;
                return map[af];
            }
        }

        public ReadOnlyCollection<int> ActionCnfValues
        {
            get
            {
                return new ReadOnlyCollection<int>(this.mReversActionMap.Keys.ToList());
            }
        }

        public ReadOnlyCollection<int> GetPredicateCnfValues(int timeStep)
        {
            return new ReadOnlyCollection<int>(this.mPredicateVariableMap[timeStep].Values.ToList());
        }

        public Operator GetOperator(int cnfValue)
        {
			if(this.mReversActionMap.ContainsKey((int)Math.Abs(cnfValue)))
				return this.mReversActionMap[(int)Math.Abs(cnfValue)];
        	return null;
		}

        public AtomicFormula GetAtomicFormula(int cnfValue)
        {
            if(this.mReversePredicateMap.ContainsKey((int)Math.Abs(cnfValue)))
				return this.mReversePredicateMap[(int)Math.Abs(cnfValue)];
			return null;
        }

        public int GetTimeStep(int cnfValue)
        {
            if(this.mTimeStepMap.ContainsKey((int)Math.Abs(cnfValue)))
				return this.mTimeStepMap[(int)Math.Abs(cnfValue)];
			return int.MinValue;
        }

    }
}
